(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
The (relative) TRS S consists of the following rules:
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
findMin(::(@x3200_4, @xs3201_4)) →+ findMin#2(findMin(@xs3201_4), @x3200_4)
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [@xs3201_4 / ::(@x3200_4, @xs3201_4)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
The (relative) TRS S consists of the following rules:
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
Rewrite Strategy: INNERMOST
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
Innermost TRS:
Rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
#compare,
findMin,
findMin#1,
minSort,
minSort#1They will be analysed ascendingly in the following order:
findMin = findMin#1
findMin < minSort
minSort = minSort#1
(8) Obligation:
Innermost TRS:
Rules:
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
findMin(
@l) →
findMin#1(
@l)
findMin#1(
::(
@x,
@xs)) →
findMin#2(
findMin(
@xs),
@x)
findMin#1(
nil) →
nilfindMin#2(
::(
@y,
@ys),
@x) →
findMin#3(
#less(
@x,
@y),
@x,
@y,
@ys)
findMin#2(
nil,
@x) →
::(
@x,
nil)
findMin#3(
#false,
@x,
@y,
@ys) →
::(
@y,
::(
@x,
@ys))
findMin#3(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
minSort(
@l) →
minSort#1(
findMin(
@l))
minSort#1(
::(
@x,
@xs)) →
::(
@x,
minSort(
@xs))
minSort#1(
nil) →
nil#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil
Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))
The following defined symbols remain to be analysed:
#compare, findMin, findMin#1, minSort, minSort#1
They will be analysed ascendingly in the following order:
findMin = findMin#1
findMin < minSort
minSort = minSort#1
(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
#compare(
gen_#0:#neg:#pos:#s5_4(
n8_4),
gen_#0:#neg:#pos:#s5_4(
n8_4)) →
#EQ, rt ∈ Ω(0)
Induction Base:
#compare(gen_#0:#neg:#pos:#s5_4(0), gen_#0:#neg:#pos:#s5_4(0)) →RΩ(0)
#EQ
Induction Step:
#compare(gen_#0:#neg:#pos:#s5_4(+(n8_4, 1)), gen_#0:#neg:#pos:#s5_4(+(n8_4, 1))) →RΩ(0)
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) →IH
#EQ
We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n0).
(10) Complex Obligation (BEST)
(11) Obligation:
Innermost TRS:
Rules:
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
findMin(
@l) →
findMin#1(
@l)
findMin#1(
::(
@x,
@xs)) →
findMin#2(
findMin(
@xs),
@x)
findMin#1(
nil) →
nilfindMin#2(
::(
@y,
@ys),
@x) →
findMin#3(
#less(
@x,
@y),
@x,
@y,
@ys)
findMin#2(
nil,
@x) →
::(
@x,
nil)
findMin#3(
#false,
@x,
@y,
@ys) →
::(
@y,
::(
@x,
@ys))
findMin#3(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
minSort(
@l) →
minSort#1(
findMin(
@l))
minSort#1(
::(
@x,
@xs)) →
::(
@x,
minSort(
@xs))
minSort#1(
nil) →
nil#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil
Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))
The following defined symbols remain to be analysed:
findMin#1, findMin, minSort, minSort#1
They will be analysed ascendingly in the following order:
findMin = findMin#1
findMin < minSort
minSort = minSort#1
(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
findMin#1(
gen_:::nil6_4(
n318853_4)) →
*7_4, rt ∈ Ω(n318853
4)
Induction Base:
findMin#1(gen_:::nil6_4(0))
Induction Step:
findMin#1(gen_:::nil6_4(+(n318853_4, 1))) →RΩ(1)
findMin#2(findMin(gen_:::nil6_4(n318853_4)), #0) →RΩ(1)
findMin#2(findMin#1(gen_:::nil6_4(n318853_4)), #0) →IH
findMin#2(*7_4, #0)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(13) Complex Obligation (BEST)
(14) Obligation:
Innermost TRS:
Rules:
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
findMin(
@l) →
findMin#1(
@l)
findMin#1(
::(
@x,
@xs)) →
findMin#2(
findMin(
@xs),
@x)
findMin#1(
nil) →
nilfindMin#2(
::(
@y,
@ys),
@x) →
findMin#3(
#less(
@x,
@y),
@x,
@y,
@ys)
findMin#2(
nil,
@x) →
::(
@x,
nil)
findMin#3(
#false,
@x,
@y,
@ys) →
::(
@y,
::(
@x,
@ys))
findMin#3(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
minSort(
@l) →
minSort#1(
findMin(
@l))
minSort#1(
::(
@x,
@xs)) →
::(
@x,
minSort(
@xs))
minSort#1(
nil) →
nil#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil
Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n318853_4)) → *7_4, rt ∈ Ω(n3188534)
Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))
The following defined symbols remain to be analysed:
findMin, minSort, minSort#1
They will be analysed ascendingly in the following order:
findMin = findMin#1
findMin < minSort
minSort = minSort#1
(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
findMin(
gen_:::nil6_4(
n321980_4)) →
*7_4, rt ∈ Ω(n321980
4)
Induction Base:
findMin(gen_:::nil6_4(0))
Induction Step:
findMin(gen_:::nil6_4(+(n321980_4, 1))) →RΩ(1)
findMin#1(gen_:::nil6_4(+(n321980_4, 1))) →RΩ(1)
findMin#2(findMin(gen_:::nil6_4(n321980_4)), #0) →IH
findMin#2(*7_4, #0)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(16) Complex Obligation (BEST)
(17) Obligation:
Innermost TRS:
Rules:
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
findMin(
@l) →
findMin#1(
@l)
findMin#1(
::(
@x,
@xs)) →
findMin#2(
findMin(
@xs),
@x)
findMin#1(
nil) →
nilfindMin#2(
::(
@y,
@ys),
@x) →
findMin#3(
#less(
@x,
@y),
@x,
@y,
@ys)
findMin#2(
nil,
@x) →
::(
@x,
nil)
findMin#3(
#false,
@x,
@y,
@ys) →
::(
@y,
::(
@x,
@ys))
findMin#3(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
minSort(
@l) →
minSort#1(
findMin(
@l))
minSort#1(
::(
@x,
@xs)) →
::(
@x,
minSort(
@xs))
minSort#1(
nil) →
nil#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil
Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n318853_4)) → *7_4, rt ∈ Ω(n3188534)
findMin(gen_:::nil6_4(n321980_4)) → *7_4, rt ∈ Ω(n3219804)
Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))
The following defined symbols remain to be analysed:
findMin#1, minSort, minSort#1
They will be analysed ascendingly in the following order:
findMin = findMin#1
findMin < minSort
minSort = minSort#1
(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
findMin#1(
gen_:::nil6_4(
n326993_4)) →
*7_4, rt ∈ Ω(n326993
4)
Induction Base:
findMin#1(gen_:::nil6_4(0))
Induction Step:
findMin#1(gen_:::nil6_4(+(n326993_4, 1))) →RΩ(1)
findMin#2(findMin(gen_:::nil6_4(n326993_4)), #0) →RΩ(1)
findMin#2(findMin#1(gen_:::nil6_4(n326993_4)), #0) →IH
findMin#2(*7_4, #0)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(19) Complex Obligation (BEST)
(20) Obligation:
Innermost TRS:
Rules:
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
findMin(
@l) →
findMin#1(
@l)
findMin#1(
::(
@x,
@xs)) →
findMin#2(
findMin(
@xs),
@x)
findMin#1(
nil) →
nilfindMin#2(
::(
@y,
@ys),
@x) →
findMin#3(
#less(
@x,
@y),
@x,
@y,
@ys)
findMin#2(
nil,
@x) →
::(
@x,
nil)
findMin#3(
#false,
@x,
@y,
@ys) →
::(
@y,
::(
@x,
@ys))
findMin#3(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
minSort(
@l) →
minSort#1(
findMin(
@l))
minSort#1(
::(
@x,
@xs)) →
::(
@x,
minSort(
@xs))
minSort#1(
nil) →
nil#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil
Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n326993_4)) → *7_4, rt ∈ Ω(n3269934)
findMin(gen_:::nil6_4(n321980_4)) → *7_4, rt ∈ Ω(n3219804)
Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))
The following defined symbols remain to be analysed:
minSort#1, minSort
They will be analysed ascendingly in the following order:
minSort = minSort#1
(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol minSort#1.
(22) Obligation:
Innermost TRS:
Rules:
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
findMin(
@l) →
findMin#1(
@l)
findMin#1(
::(
@x,
@xs)) →
findMin#2(
findMin(
@xs),
@x)
findMin#1(
nil) →
nilfindMin#2(
::(
@y,
@ys),
@x) →
findMin#3(
#less(
@x,
@y),
@x,
@y,
@ys)
findMin#2(
nil,
@x) →
::(
@x,
nil)
findMin#3(
#false,
@x,
@y,
@ys) →
::(
@y,
::(
@x,
@ys))
findMin#3(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
minSort(
@l) →
minSort#1(
findMin(
@l))
minSort#1(
::(
@x,
@xs)) →
::(
@x,
minSort(
@xs))
minSort#1(
nil) →
nil#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil
Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n326993_4)) → *7_4, rt ∈ Ω(n3269934)
findMin(gen_:::nil6_4(n321980_4)) → *7_4, rt ∈ Ω(n3219804)
Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))
The following defined symbols remain to be analysed:
minSort
They will be analysed ascendingly in the following order:
minSort = minSort#1
(23) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol minSort.
(24) Obligation:
Innermost TRS:
Rules:
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
findMin(
@l) →
findMin#1(
@l)
findMin#1(
::(
@x,
@xs)) →
findMin#2(
findMin(
@xs),
@x)
findMin#1(
nil) →
nilfindMin#2(
::(
@y,
@ys),
@x) →
findMin#3(
#less(
@x,
@y),
@x,
@y,
@ys)
findMin#2(
nil,
@x) →
::(
@x,
nil)
findMin#3(
#false,
@x,
@y,
@ys) →
::(
@y,
::(
@x,
@ys))
findMin#3(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
minSort(
@l) →
minSort#1(
findMin(
@l))
minSort#1(
::(
@x,
@xs)) →
::(
@x,
minSort(
@xs))
minSort#1(
nil) →
nil#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil
Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n326993_4)) → *7_4, rt ∈ Ω(n3269934)
findMin(gen_:::nil6_4(n321980_4)) → *7_4, rt ∈ Ω(n3219804)
Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))
No more defined symbols left to analyse.
(25) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
findMin#1(gen_:::nil6_4(n326993_4)) → *7_4, rt ∈ Ω(n3269934)
(26) BOUNDS(n^1, INF)
(27) Obligation:
Innermost TRS:
Rules:
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
findMin(
@l) →
findMin#1(
@l)
findMin#1(
::(
@x,
@xs)) →
findMin#2(
findMin(
@xs),
@x)
findMin#1(
nil) →
nilfindMin#2(
::(
@y,
@ys),
@x) →
findMin#3(
#less(
@x,
@y),
@x,
@y,
@ys)
findMin#2(
nil,
@x) →
::(
@x,
nil)
findMin#3(
#false,
@x,
@y,
@ys) →
::(
@y,
::(
@x,
@ys))
findMin#3(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
minSort(
@l) →
minSort#1(
findMin(
@l))
minSort#1(
::(
@x,
@xs)) →
::(
@x,
minSort(
@xs))
minSort#1(
nil) →
nil#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil
Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n326993_4)) → *7_4, rt ∈ Ω(n3269934)
findMin(gen_:::nil6_4(n321980_4)) → *7_4, rt ∈ Ω(n3219804)
Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))
No more defined symbols left to analyse.
(28) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
findMin#1(gen_:::nil6_4(n326993_4)) → *7_4, rt ∈ Ω(n3269934)
(29) BOUNDS(n^1, INF)
(30) Obligation:
Innermost TRS:
Rules:
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
findMin(
@l) →
findMin#1(
@l)
findMin#1(
::(
@x,
@xs)) →
findMin#2(
findMin(
@xs),
@x)
findMin#1(
nil) →
nilfindMin#2(
::(
@y,
@ys),
@x) →
findMin#3(
#less(
@x,
@y),
@x,
@y,
@ys)
findMin#2(
nil,
@x) →
::(
@x,
nil)
findMin#3(
#false,
@x,
@y,
@ys) →
::(
@y,
::(
@x,
@ys))
findMin#3(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
minSort(
@l) →
minSort#1(
findMin(
@l))
minSort#1(
::(
@x,
@xs)) →
::(
@x,
minSort(
@xs))
minSort#1(
nil) →
nil#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil
Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n318853_4)) → *7_4, rt ∈ Ω(n3188534)
findMin(gen_:::nil6_4(n321980_4)) → *7_4, rt ∈ Ω(n3219804)
Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))
No more defined symbols left to analyse.
(31) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
findMin#1(gen_:::nil6_4(n318853_4)) → *7_4, rt ∈ Ω(n3188534)
(32) BOUNDS(n^1, INF)
(33) Obligation:
Innermost TRS:
Rules:
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
findMin(
@l) →
findMin#1(
@l)
findMin#1(
::(
@x,
@xs)) →
findMin#2(
findMin(
@xs),
@x)
findMin#1(
nil) →
nilfindMin#2(
::(
@y,
@ys),
@x) →
findMin#3(
#less(
@x,
@y),
@x,
@y,
@ys)
findMin#2(
nil,
@x) →
::(
@x,
nil)
findMin#3(
#false,
@x,
@y,
@ys) →
::(
@y,
::(
@x,
@ys))
findMin#3(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
minSort(
@l) →
minSort#1(
findMin(
@l))
minSort#1(
::(
@x,
@xs)) →
::(
@x,
minSort(
@xs))
minSort#1(
nil) →
nil#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil
Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n318853_4)) → *7_4, rt ∈ Ω(n3188534)
Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))
No more defined symbols left to analyse.
(34) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
findMin#1(gen_:::nil6_4(n318853_4)) → *7_4, rt ∈ Ω(n3188534)
(35) BOUNDS(n^1, INF)
(36) Obligation:
Innermost TRS:
Rules:
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
findMin(
@l) →
findMin#1(
@l)
findMin#1(
::(
@x,
@xs)) →
findMin#2(
findMin(
@xs),
@x)
findMin#1(
nil) →
nilfindMin#2(
::(
@y,
@ys),
@x) →
findMin#3(
#less(
@x,
@y),
@x,
@y,
@ys)
findMin#2(
nil,
@x) →
::(
@x,
nil)
findMin#3(
#false,
@x,
@y,
@ys) →
::(
@y,
::(
@x,
@ys))
findMin#3(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
minSort(
@l) →
minSort#1(
findMin(
@l))
minSort#1(
::(
@x,
@xs)) →
::(
@x,
minSort(
@xs))
minSort#1(
nil) →
nil#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil
Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))
No more defined symbols left to analyse.
(37) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(1) was proven with the following lemma:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
(38) BOUNDS(1, INF)